2022年优秀学位论文展（7-1）丨 软件工程：金鹏/硕士
—— 2022年度 ——
优秀学位论文展
博士
学硕
专硕
学位论文是研究生培养质量的重要标志，自2021年起，我校建立校级优秀学位论文评选制度，激发研究生潜心学术，激励导师悉心指导研究生。2022年度，206篇论文入选华东师范大学研究生优秀学位论文。
今天，就让我们一同走近
2022年度优秀硕士学位论文获得者
金 鹏
01
人物简介
01
论文中文题目
基于抽象域训练的可验证强化学习
02
论文英文题目
Verifiable Reinforcement Learning by Training on Abstract Domains
03
指导教师
张民 教授
04
培养院系
软件工程学院
05
所属一级学科
软件工程
06
读研感言
《传习录》中有片段：“立志用功，如种树然。方其根芽，犹未有干; 及其有干，尚未有枝；枝而后叶，叶而后花、实。初种根时，只管栽培灌溉，勿作枝想，勿作叶想，勿作花想，勿作实想。悬想何益?但不忘栽培之功，怕没有枝叶花实?”
三年不短，能够沉下心从一而终，想来还是会有所收获的。
02
学位论文信息
01
论文研究背景/选题意义/研究价值
自20世纪50年代，机器学习逐渐被深入研究，并在近几年被应用于多样的现实场景中。特别是在医学影像、自动驾驶和人脸识别等重要方向的应用中，机器学习展现出了极大的潜力。作为机器学习的一个子领域产物，深度学习在其中扮演了关键的角色，这得益于其所依赖的底层模型，即深度神经网络的飞速发展。更重要的是，神经网络的独特优势使得它也被作为除监督学习外其他学习方式的底层模型，并推动了相关领域的进步。其中最为突出的就是深度强化学习，这也是本文关注的重点。
但是Szegedy等人在2013年发表的论文中首次揭示了神经网络存在的客观缺陷。具体来说，在图像分类的场景中，受到微小噪声扰动的图像会被神经网络判定为与原图像不同的类别标签，即使扰动对于人类来说无法察觉。而其中能够干扰神经网络决策的噪声图像被称为对抗样本，攻击者可以通过构造对抗样本，并将其作为输入，以轻易地攻击基于神经网络的应用。该缺陷无疑会影响神经网络在安全攸关领域中的进一步应用，因而截止目前，关于如何解决神经网络因对抗样本表现出的不鲁棒性的研究仍然是公开的热点问题。目前的解决方法大致可以被分为三类：(1)鲁棒性训练：通过修改损失函数或在训练集中加入对抗样本以生成更为鲁棒的神经网络；(2)辅助决策：引入额外的方法或模型辅助神经网络决策；(3)形式化验证：通过线性规划、可满足性模块理论或抽象解释等形式化方法计算神经网络对于特定输入样本的鲁棒半径。
但是上述针对监督学习中神经网络的形式化验证方法无法被直接迁移到深度强化学习所应用的场景中，即使二者依赖的底层模型相同。因此能够解决该问题的方法必定会对强化学习系统甚至是其他由神经网络驱动的系统的进一步应用带来积极的意义。首先是因为目前深度强化学习在安全攸关领域的应用存在明显的瓶颈。例如其是否能完全解决在自动驾驶领 域中遇到的应用问题就引发了许多争论。即使目前所提出的形式化方法所能够处理的系统规模与落地应用还不在一个层面上，其核心思想也能启发实际应用的工作。其次，相较于针对神经网络单次决策的鲁棒性验证，验证系统层面性质更能保障其在部署场景下的行为可控性。最后，如验证方法能够将神经网络作为“黑盒”模型处理，即验证方法的可扩展性不受制于神经网络的各种性质 (比如神经网络的规模与结构)，就能增加将验证方法运用到其他由神经网络驱动的系统的可行性。
02
主要研究内容
深度强化学习是一种极具前景的技术，可用于解决现实场景中的各种复杂控制问题。然而，强化学习系统具有的三个特性使得验证工作变得十分困难，其中这三个特性分别是：(1) 系统通常具有连续的状态空间；(2) 系统的状态转移方程一般是非线性的；(3) 部署在系统中的深度神经网络是不可解释的。因此，在缺乏有效的验证方法来确保可靠性的前提下，强化学习在安全攸关领域中的应用受到了一定的限制。
为了缓解该现状，本文提出了一种通过在包含有限抽象状态的抽象域上训练神经网络来实现可验证强化学习的新方法。通过该方法训练的神经网络能够满足两个关键的需求。首先是其性能与通过传统算法训练生成的神经网络相近。此外，神经网络的决策域是有限的，因此可以利用现有的模型检测技术来验证由它驱动的强化学习系统。
本文实现了一个训练及验证框架，它具有三个独特的优势：(1) 基于抽象域的训练技术与现有的大多数强化学习训练算法互不影响，因此其可被应用于主流的算法中；(2) 神经网络的规模和结构不会限制验证方法的可扩展性；(3) 支持在有扰动的情况下验证系统的时序性质。
本文基于该框架对五个经典的控制系统进行了完备的实验。实验结果表明，基于本文的方法能够有效地验证这些系统的复杂时序性质。同时，与传统算法训练生成的控制系统相比，它们能够保持对应的基准性能。更重要的是，在与现有最先进的验证强化学习系统工具的对比实验中，该框架也表现出了良好的可扩展性与广泛的可应用性。
03
主要创新点
主要作出了如下的三个贡献：
1）创新性地提出了一种在有限的抽象域上训练神经网络的强化学习技术， 由此生成的神经网络可使对应的控制系统被直接验证。
2）实现了一个基于抽象训练技术的强化学习训练及验证框架。该框架能够形式化验证控制系统的复杂时序性质。
3）提供了大量的关于测试控制系统的实验数据，包括基于抽象域的训练 表现与相应的验证结果，这将有助于后续工作进行对比与评估。
03
代表性创新成果
01
在第34届Computer Aided Verification会议发表论文《Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning》。
02
在第34届Software Engineering & Knowledge Engineering会议发表论文《Efficient LTL Model Checking of Deep Reinforcement Learning Systems using Policy Extraction》。
04
导师
01
导师简介
张民，软件工程学院教授，博士生导师。研究方向为可信软件、可信人工智能和分布式系统。研究受到国家自然基金委国际合作项目、面上项目、华为全球创新研究计划等项目资助，2019年入选中法“蔡元培”人才培养计划及法国尼斯大学高级访问教授计划。代表性论文发表在CAV、AAAI、OOPSLA、ASE、RTSS等国际顶级会议上。获得第26届IEEE亚太软件工程会议APSEC唯一最佳论文奖，FSE2020、 RE2019和ASE2022会议最佳论文提名奖。在研究生培养中尊重学生的兴趣，鼓励学生自由探索，挑战难题，同学生一起教学相长。
02
导师对该生的评价
金鹏同学科研上非常踏实，爱钻研，在研究上有自己的见解，动手能力强。我们一开始就选择了国际上比较有挑战的强化学习系统的训练与形式化验证问题，金鹏同学做了大量的文献调研，经过多次交流讨论，我们首次提出通过抽象技术训练和验证深度强化学习系统，得到很好的实验结果。虽然论文发表并不顺利，数次被拒稿。我们不断继续完善提出的方法和实验，最后论文发表在计算机理论顶级会议CAV上。精诚所至，金石为开，鲲鹏展翅，翱翔天际。三年科研历练，相信会帮助金鹏同学会在今后的工作中发展越来越好！